Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(x1)))

Q is empty.


QTRS
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

a(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(x1)))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

a(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(x1)))

The set Q is empty.
We have obtained the following QTRS:

a(c(a(x))) → c(a(c(x)))
b(a(a(x))) → b(d(a(x)))
b(a(x)) → a(a(b(x)))
d(d(x)) → b(d(a(x)))
b(b(x)) → c(b(x))
c(d(a(x))) → a(c(x))
c(b(x)) → a(a(a(x)))

The set Q is empty.

↳ QTRS
  ↳ QTRS Reverse
QTRS
      ↳ RFCMatchBoundsTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a(c(a(x))) → c(a(c(x)))
b(a(a(x))) → b(d(a(x)))
b(a(x)) → a(a(b(x)))
d(d(x)) → b(d(a(x)))
b(b(x)) → c(b(x))
c(d(a(x))) → a(c(x))
c(b(x)) → a(a(a(x)))

Q is empty.

Termination of the TRS R could be shown with a Match Bound [6,7] of 4. This implies Q-termination of R.
The following rules were used to construct the certificate:

a(c(a(x))) → c(a(c(x)))
b(a(a(x))) → b(d(a(x)))
b(a(x)) → a(a(b(x)))
d(d(x)) → b(d(a(x)))
b(b(x)) → c(b(x))
c(d(a(x))) → a(c(x))
c(b(x)) → a(a(a(x)))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

108, 109, 110, 112, 111, 113, 114, 115, 117, 116, 119, 118, 120, 121, 123, 122, 125, 124, 127, 126, 129, 128, 131, 130, 133, 132, 135, 134, 137, 136, 139, 138, 141, 140, 143, 142, 145, 144, 168, 167

Node 108 is start node and node 109 is final node.

Those nodes are connect through the following edges: